Termination w.r.t. Q of the following Term Rewriting System could not be shown:
Q restricted rewrite system:
The TRS R consists of the following rules:
sum(cons(s(n), x), cons(m, y)) → sum(cons(n, x), cons(s(m), y))
sum(cons(0, x), y) → sum(x, y)
sum(nil, y) → y
weight(cons(n, cons(m, x))) → weight(sum(cons(n, cons(m, x)), cons(0, x)))
weight(cons(n, nil)) → n
Q is empty.
↳ QTRS
Q restricted rewrite system:
The TRS R consists of the following rules:
sum(cons(s(n), x), cons(m, y)) → sum(cons(n, x), cons(s(m), y))
sum(cons(0, x), y) → sum(x, y)
sum(nil, y) → y
weight(cons(n, cons(m, x))) → weight(sum(cons(n, cons(m, x)), cons(0, x)))
weight(cons(n, nil)) → n
Q is empty.